\begin{tabbing}
$\forall$${\it es}$:ES, $L$:(Id List).
\\[0ex]fischer($L$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]fEvent($e$)
\\[0ex]$\Rightarrow$ \=($\forall$$i$:$\mathbb{N}$.\+
\\[0ex](\=$\forall$$j$:$\mathbb{N}$.\+
\\[0ex](\=(rank($e$) = $<$$i$, (2 $\ast$ $j$)+1$>$ $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$))\+
\\[0ex]$\Rightarrow$ ((("x" after $e$) = "try" $\in$ Id) $\vee$ (("x" after $e$) = "taken" $\in$ Id)))
\-\\[0ex]\& (\=(rank($e$) = $<$$i$, (2 $\ast$ $j$)+2$>$ $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$))\+
\\[0ex]$\Rightarrow$ ((("x" after $e$) = "contending" $\in$ Id) $\vee$ (("x" after $e$) = "mine" $\in$ Id))))
\-\-\\[0ex]\& ((rank($e$) = $<$$i$, 0$>$ $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$)) $\Rightarrow$ (("x" after $e$) = "free" $\in$ Id \& (0 $<$ $i$)))))
\-\-
\end{tabbing}